<!DOCTYPE html>
<html lang="zh-CN">
<head>
  <meta charset="UTF-8">
<meta name="viewport" content="width=device-width">
<meta name="theme-color" content="#222"><meta name="generator" content="Hexo 6.3.0">

  <link rel="apple-touch-icon" sizes="180x180" href="/blog/images/apple-touch-icon-next.png">
  <link rel="icon" type="image/png" sizes="32x32" href="/blog/images/Horse.png">
  <link rel="icon" type="image/png" sizes="16x16" href="/blog/images/Horse.png">
  <link rel="mask-icon" href="/blog/images/logo.svg" color="#222">

<link rel="stylesheet" href="/blog/css/main.css">



<link rel="stylesheet" href="https://cdnjs.cloudflare.com/ajax/libs/font-awesome/6.4.0/css/all.min.css" integrity="sha256-HtsXJanqjKTc8vVQjO4YMhiqFoXkfBsjBWcX91T1jr8=" crossorigin="anonymous">
  <link rel="stylesheet" href="https://cdnjs.cloudflare.com/ajax/libs/fancybox/3.5.7/jquery.fancybox.min.css" integrity="sha256-Vzbj7sDDS/woiFS3uNKo8eIuni59rjyNGtXfstRzStA=" crossorigin="anonymous">

<script class="next-config" data-name="main" type="application/json">{"hostname":"yanlwsometing.gitee.io","root":"/blog/","images":"/blog/images","scheme":"Pisces","darkmode":false,"version":"8.16.0","exturl":false,"sidebar":{"position":"left","display":"post","padding":18,"offset":12},"copycode":{"enable":true,"show_result":true,"style":"flat"},"bookmark":{"enable":false,"color":"#222","save":"auto"},"mediumzoom":false,"lazyload":false,"pangu":false,"comments":{"style":"tabs","active":null,"storage":true,"lazyload":false,"nav":null},"stickytabs":false,"motion":{"enable":false,"async":false,"transition":{"menu_item":"fadeInDown","post_block":"fadeIn","post_header":"fadeInDown","post_body":"fadeInDown","coll_header":"fadeInLeft","sidebar":"fadeInUp"}},"prism":false,"i18n":{"placeholder":"搜索...","empty":"没有找到任何搜索结果：${query}","hits_time":"找到 ${hits} 个搜索结果（用时 ${time} 毫秒）","hits":"找到 ${hits} 个搜索结果"}}</script><script src="/blog/js/config.js"></script>

    <meta name="description" content="多态（Polymorphism）多态，即面对不同类型的数据，同一种方法具有不同的表现形式 1.  多态列表(Polymorphic Lists)在Lists章中，我们创建了自然数类型的列表，但我们需要不同类型的列表就要重新创建，因此我们需要“多态列表” 123Inductive list (X:Type) : Type :&#x3D;  | nil  | cons (x : X) (l : list X).">
<meta property="og:type" content="article">
<meta property="og:title" content="SF-1-Poly">
<meta property="og:url" content="https://yanlwsometing.gitee.io/blog/2023/07/19/SF-1-Poly/index.html">
<meta property="og:site_name" content="yanlwsometing">
<meta property="og:description" content="多态（Polymorphism）多态，即面对不同类型的数据，同一种方法具有不同的表现形式 1.  多态列表(Polymorphic Lists)在Lists章中，我们创建了自然数类型的列表，但我们需要不同类型的列表就要重新创建，因此我们需要“多态列表” 123Inductive list (X:Type) : Type :&#x3D;  | nil  | cons (x : X) (l : list X).">
<meta property="og:locale" content="zh_CN">
<meta property="article:published_time" content="2023-07-19T09:19:00.000Z">
<meta property="article:modified_time" content="2023-12-15T09:08:38.579Z">
<meta property="article:author" content="yanlw">
<meta property="article:tag" content="博客">
<meta name="twitter:card" content="summary">


<link rel="canonical" href="https://yanlwsometing.gitee.io/blog/2023/07/19/SF-1-Poly/">



<script class="next-config" data-name="page" type="application/json">{"sidebar":"","isHome":false,"isPost":true,"lang":"zh-CN","comments":true,"permalink":"https://yanlwsometing.gitee.io/blog/2023/07/19/SF-1-Poly/","path":"2023/07/19/SF-1-Poly/","title":"SF-1-Poly"}</script>

<script class="next-config" data-name="calendar" type="application/json">""</script>
<title>SF-1-Poly | yanlwsometing</title>
  








  <noscript>
    <link rel="stylesheet" href="/blog/css/noscript.css">
  </noscript>
</head>

<body itemscope itemtype="http://schema.org/WebPage">
  <div class="headband"></div>

  <main class="main">
    <div class="column">
      <header class="header" itemscope itemtype="http://schema.org/WPHeader"><div class="site-brand-container">
  <div class="site-nav-toggle">
    <div class="toggle" aria-label="切换导航栏" role="button">
        <span class="toggle-line"></span>
        <span class="toggle-line"></span>
        <span class="toggle-line"></span>
    </div>
  </div>

  <div class="site-meta">

    <a href="/blog/" class="brand" rel="start">
      <i class="logo-line"></i>
      <p class="site-title">yanlwsometing</p>
      <i class="logo-line"></i>
    </a>
  </div>

  <div class="site-nav-right">
    <div class="toggle popup-trigger" aria-label="搜索" role="button">
    </div>
  </div>
</div>



<nav class="site-nav">
  <ul class="main-menu menu"><li class="menu-item menu-item-home"><a href="/blog/" rel="section"><i class="fa fa-home fa-fw"></i>首页</a></li><li class="menu-item menu-item-tags"><a href="/blog/tags/" rel="section"><i class="fa fa-tags fa-fw"></i>标签</a></li><li class="menu-item menu-item-categories"><a href="/blog/categories/" rel="section"><i class="fa fa-th fa-fw"></i>分类</a></li><li class="menu-item menu-item-archives"><a href="/blog/archives/" rel="section"><i class="fa fa-archive fa-fw"></i>归档</a></li><li class="menu-item menu-item-commonweal"><a href="/blog/404/" rel="section"><i class="fa fa-heartbeat fa-fw"></i>公益 404</a></li>
  </ul>
</nav>




</header>
        
  
  <aside class="sidebar">

    <div class="sidebar-inner sidebar-nav-active sidebar-toc-active">
      <ul class="sidebar-nav">
        <li class="sidebar-nav-toc">
          文章目录
        </li>
        <li class="sidebar-nav-overview">
          站点概览
        </li>
      </ul>

      <div class="sidebar-panel-container">
        <!--noindex-->
        <div class="post-toc-wrap sidebar-panel">
            <div class="post-toc animated"><ol class="nav"><li class="nav-item nav-level-2"><a class="nav-link" href="#%E5%A4%9A%E6%80%81%EF%BC%88Polymorphism%EF%BC%89"><span class="nav-number">1.</span> <span class="nav-text">多态（Polymorphism）</span></a><ol class="nav-child"><li class="nav-item nav-level-3"><a class="nav-link" href="#1-%E5%A4%9A%E6%80%81%E5%88%97%E8%A1%A8-Polymorphic-Lists"><span class="nav-number">1.1.</span> <span class="nav-text">1.  多态列表(Polymorphic Lists)</span></a><ol class="nav-child"><li class="nav-item nav-level-4"><a class="nav-link" href="#%E7%B1%BB%E5%9E%8B%E6%A0%87%E6%B3%A8%E7%9A%84%E6%8E%A8%E6%96%AD-Type-Annotation-Inference"><span class="nav-number">1.1.1.</span> <span class="nav-text">类型标注的推断(Type Annotation Inference)</span></a></li><li class="nav-item nav-level-4"><a class="nav-link" href="#%E7%B1%BB%E5%9E%8B%E5%8F%82%E6%95%B0%E7%9A%84%E6%8E%A8%E6%96%AD-Type-Argument-Synthesis"><span class="nav-number">1.1.2.</span> <span class="nav-text">类型参数的推断(Type Argument Synthesis)</span></a></li><li class="nav-item nav-level-4"><a class="nav-link" href="#%E9%9A%90%E5%BC%8F%E5%8F%82%E6%95%B0%EF%BC%88Implicit-Arguments%EF%BC%89"><span class="nav-number">1.1.3.</span> <span class="nav-text">隐式参数（Implicit Arguments）</span></a></li><li class="nav-item nav-level-4"><a class="nav-link" href="#%E6%98%BE%E5%BC%8F%E6%8F%90%E4%BE%9B%E7%B1%BB%E5%9E%8B%E5%8F%82%E6%95%B0"><span class="nav-number">1.1.4.</span> <span class="nav-text">显式提供类型参数</span></a></li></ol></li><li class="nav-item nav-level-3"><a class="nav-link" href="#2-%E5%A4%9A%E6%80%81%E5%BA%8F%E5%AF%B9"><span class="nav-number">1.2.</span> <span class="nav-text">2.  多态序对</span></a></li><li class="nav-item nav-level-3"><a class="nav-link" href="#3-%E5%A4%9A%E6%80%81%E5%80%99%E9%80%89"><span class="nav-number">1.3.</span> <span class="nav-text">3.  多态候选</span></a></li></ol></li><li class="nav-item nav-level-2"><a class="nav-link" href="#%E5%87%BD%E6%95%B0%E4%BD%9C%E4%B8%BA%E6%95%B0%E6%8D%AE%EF%BC%88Functions-as-Data%EF%BC%89"><span class="nav-number">2.</span> <span class="nav-text">函数作为数据（Functions as Data）</span></a><ol class="nav-child"><li class="nav-item nav-level-3"><a class="nav-link" href="#1-filter"><span class="nav-number">2.1.</span> <span class="nav-text">1. filter</span></a></li><li class="nav-item nav-level-3"><a class="nav-link" href="#2-map"><span class="nav-number">2.2.</span> <span class="nav-text">2. map</span></a></li><li class="nav-item nav-level-3"><a class="nav-link" href="#3-fold"><span class="nav-number">2.3.</span> <span class="nav-text">3. fold</span></a></li><li class="nav-item nav-level-3"><a class="nav-link" href="#4-%E5%8C%BF%E5%90%8D%E5%87%BD%E6%95%B0-Anonymous-Functions"><span class="nav-number">2.4.</span> <span class="nav-text">4. 匿名函数(Anonymous Functions)</span></a></li></ol></li><li class="nav-item nav-level-2"><a class="nav-link" href="#Exercises"><span class="nav-number">3.</span> <span class="nav-text">Exercises</span></a><ol class="nav-child"><li class="nav-item nav-level-3"><a class="nav-link" href="#1-Exercise-2-stars-standard-fold-length"><span class="nav-number">3.1.</span> <span class="nav-text">1. Exercise: 2 stars, standard (fold_length)</span></a></li><li class="nav-item nav-level-3"><a class="nav-link" href="#2-Exercise-2-stars-advanced-currying"><span class="nav-number">3.2.</span> <span class="nav-text">2. Exercise: 2 stars, advanced (currying)</span></a></li><li class="nav-item nav-level-3"><a class="nav-link" href="#3-Church-Numerals-Advanced"><span class="nav-number">3.3.</span> <span class="nav-text">3. Church Numerals (Advanced)</span></a></li></ol></li></ol></div>
        </div>
        <!--/noindex-->

        <div class="site-overview-wrap sidebar-panel">
          <div class="site-author animated" itemprop="author" itemscope itemtype="http://schema.org/Person">
    <img class="site-author-image" itemprop="image" alt="yanlw"
      src="/blog/images/avatar.jpg">
  <p class="site-author-name" itemprop="name">yanlw</p>
  <div class="site-description" itemprop="description">穷则独善其身，达则兼济天下！</div>
</div>
<div class="site-state-wrap animated">
  <nav class="site-state">
      <div class="site-state-item site-state-posts">
        <a href="/blog/archives/">
          <span class="site-state-item-count">23</span>
          <span class="site-state-item-name">日志</span>
        </a>
      </div>
      <div class="site-state-item site-state-categories">
          <a href="/blog/categories/">
        <span class="site-state-item-count">9</span>
        <span class="site-state-item-name">分类</span></a>
      </div>
      <div class="site-state-item site-state-tags">
          <a href="/blog/tags/">
        <span class="site-state-item-count">18</span>
        <span class="site-state-item-name">标签</span></a>
      </div>
  </nav>
</div>
  <div class="links-of-author animated">
      <span class="links-of-author-item">
        <a href="https://gitee.com/yanlwsometing" title="Gitee → https:&#x2F;&#x2F;gitee.com&#x2F;yanlwsometing" rel="noopener me" target="_blank"><i class="fab fa-gitee fa-fw"></i>Gitee</a>
      </span>
      <span class="links-of-author-item">
        <a href="mailto:1977712019@qq.com" title="Mail → mailto:1977712019@qq.com" rel="noopener me" target="_blank"><i class="fa fa-envelope fa-fw"></i>Mail</a>
      </span>
      <span class="links-of-author-item">
        <a href="https://weibo.com/" title="Weibo → https:&#x2F;&#x2F;weibo.com&#x2F;" rel="noopener me" target="_blank"><i class="fab fa-weibo fa-fw"></i>Weibo</a>
      </span>
      <span class="links-of-author-item">
        <a href="https://twitter.com/" title="Twitter → https:&#x2F;&#x2F;twitter.com&#x2F;" rel="noopener me" target="_blank"><i class="fab fa-twitter fa-fw"></i>Twitter</a>
      </span>
  </div>

        </div>
      </div>
        <div class="back-to-top animated" role="button" aria-label="返回顶部">
          <i class="fa fa-arrow-up"></i>
          <span>0%</span>
        </div>
    </div>

    
  </aside>


    </div>

    <div class="main-inner post posts-expand">


  


<div class="post-block">
  
  

  <article itemscope itemtype="http://schema.org/Article" class="post-content" lang="zh-CN">
    <link itemprop="mainEntityOfPage" href="https://yanlwsometing.gitee.io/blog/2023/07/19/SF-1-Poly/">

    <span hidden itemprop="author" itemscope itemtype="http://schema.org/Person">
      <meta itemprop="image" content="/blog/images/avatar.jpg">
      <meta itemprop="name" content="yanlw">
    </span>

    <span hidden itemprop="publisher" itemscope itemtype="http://schema.org/Organization">
      <meta itemprop="name" content="yanlwsometing">
      <meta itemprop="description" content="穷则独善其身，达则兼济天下！">
    </span>

    <span hidden itemprop="post" itemscope itemtype="http://schema.org/CreativeWork">
      <meta itemprop="name" content="SF-1-Poly | yanlwsometing">
      <meta itemprop="description" content="">
    </span>
      <header class="post-header">
        <h1 class="post-title" itemprop="name headline">
          SF-1-Poly
        </h1>

        <div class="post-meta-container">
          <div class="post-meta">
    <span class="post-meta-item">
      <span class="post-meta-item-icon">
        <i class="far fa-calendar"></i>
      </span>
      <span class="post-meta-item-text">发表于</span>

      <time title="创建时间：2023-07-19 17:19:00" itemprop="dateCreated datePublished" datetime="2023-07-19T17:19:00+08:00">2023-07-19</time>
    </span>
    <span class="post-meta-item">
      <span class="post-meta-item-icon">
        <i class="far fa-calendar-check"></i>
      </span>
      <span class="post-meta-item-text">更新于</span>
      <time title="修改时间：2023-12-15 17:08:38" itemprop="dateModified" datetime="2023-12-15T17:08:38+08:00">2023-12-15</time>
    </span>
    <span class="post-meta-item">
      <span class="post-meta-item-icon">
        <i class="far fa-folder"></i>
      </span>
      <span class="post-meta-item-text">分类于</span>
        <span itemprop="about" itemscope itemtype="http://schema.org/Thing">
          <a href="/blog/categories/Coq/" itemprop="url" rel="index"><span itemprop="name">Coq</span></a>
        </span>
    </span>

  
    <span class="post-meta-item" title="阅读次数" id="busuanzi_container_page_pv">
      <span class="post-meta-item-icon">
        <i class="far fa-eye"></i>
      </span>
      <span class="post-meta-item-text">阅读次数：</span>
      <span id="busuanzi_value_page_pv"></span>
    </span>
</div>

        </div>
      </header>

    
    
    
    <div class="post-body" itemprop="articleBody"><h2 id="多态（Polymorphism）"><a href="#多态（Polymorphism）" class="headerlink" title="多态（Polymorphism）"></a>多态（Polymorphism）</h2><p>多态，即面对不同类型的数据，同一种方法具有不同的表现形式</p>
<h3 id="1-多态列表-Polymorphic-Lists"><a href="#1-多态列表-Polymorphic-Lists" class="headerlink" title="1.  多态列表(Polymorphic Lists)"></a>1.  多态列表(Polymorphic Lists)</h3><p>在Lists章中，我们创建了自然数类型的列表，但我们需要不同类型的列表就要重新创建，因此我们需要“多态列表”</p>
<figure class="highlight plaintext"><table><tr><td class="gutter"><pre><span class="line">1</span><br><span class="line">2</span><br><span class="line">3</span><br></pre></td><td class="code"><pre><span class="line">Inductive list (X:Type) : Type :=</span><br><span class="line">  | nil</span><br><span class="line">  | cons (x : X) (l : list X).</span><br></pre></td></tr></table></figure>

<p>其中，list 是个从 Type 类型到 Type 类型的函数。list 的定义中的参数 X 自动 成为构造子 nil 和 cons 的参数。至于具体的列表，它的类型为list X.</p>
<figure class="highlight plaintext"><table><tr><td class="gutter"><pre><span class="line">1</span><br></pre></td><td class="code"><pre><span class="line">Check (cons nat 3 (nil nat)) : list nat.</span><br></pre></td></tr></table></figure>

<p>其函数的多态版本如下</p>
<figure class="highlight plaintext"><table><tr><td class="gutter"><pre><span class="line">1</span><br><span class="line">2</span><br><span class="line">3</span><br><span class="line">4</span><br><span class="line">5</span><br></pre></td><td class="code"><pre><span class="line">Fixpoint repeat (X : Type) (x : X) (count : nat) : list X :=</span><br><span class="line">  match count with</span><br><span class="line">  | 0 ⇒ nil X</span><br><span class="line">  | S count&#x27; ⇒ cons X x (repeat X x count&#x27;)</span><br><span class="line">  end.</span><br></pre></td></tr></table></figure>

<span id="more"></span>

<h4 id="类型标注的推断-Type-Annotation-Inference"><a href="#类型标注的推断-Type-Annotation-Inference" class="headerlink" title="类型标注的推断(Type Annotation Inference)"></a>类型标注的推断(Type Annotation Inference)</h4><p>当不指定参数类型，Coq使用类型推断出其参数类型。</p>
<figure class="highlight plaintext"><table><tr><td class="gutter"><pre><span class="line">1</span><br><span class="line">2</span><br><span class="line">3</span><br><span class="line">4</span><br><span class="line">5</span><br></pre></td><td class="code"><pre><span class="line">Fixpoint repeat&#x27; X x count : list X :=</span><br><span class="line">  match count with</span><br><span class="line">  | 0 ⇒ nil X</span><br><span class="line">  | S count&#x27; ⇒ cons X x (repeat&#x27; X x count&#x27;)</span><br><span class="line">  end.</span><br></pre></td></tr></table></figure>

<p>例如， 由于 X 是作为 cons 的参数使用的，因此它必定是个 Type 类型， 因为 cons 期望一个 Type 作为其第一个参数，而用 0 和 S 来匹配 count 意味着它必须是个 nat，诸如此类</p>
<p><strong>注意：显式的类型标注对于文档和完整性检查来说仍然非常有用</strong></p>
<h4 id="类型参数的推断-Type-Argument-Synthesis"><a href="#类型参数的推断-Type-Argument-Synthesis" class="headerlink" title="类型参数的推断(Type Argument Synthesis)"></a>类型参数的推断(Type Argument Synthesis)</h4><p>但是，我们还希望更简单一点。例如，由于 repeat 的第二个参数为 X 类型的元素，第一个参数明显只能是 X， 既然如此，我们何必显式地写出它呢？</p>
<p>Coq 允许避免这种冗余，将类型参数写为 “_” 。<strong>当 Coq 遇到 _ 时，它会尝试*’统一’*所有的局部变量信息， 包括函数应当应用到的类型，其它参数的类型，以及应用函数的上下文中期望的类型， 以此来确定 _ 处应当填入的具体类型。</strong></p>
<figure class="highlight plaintext"><table><tr><td class="gutter"><pre><span class="line">1</span><br><span class="line">2</span><br><span class="line">3</span><br><span class="line">4</span><br><span class="line">5</span><br></pre></td><td class="code"><pre><span class="line">Fixpoint repeat&#x27;&#x27; X x count : list X :=</span><br><span class="line">  match count with</span><br><span class="line">  | 0 ⇒ nil _</span><br><span class="line">  | S count&#x27; ⇒ cons _ x (repeat&#x27;&#x27; _ x count&#x27;)</span><br><span class="line">  end.</span><br></pre></td></tr></table></figure>



<h4 id="隐式参数（Implicit-Arguments）"><a href="#隐式参数（Implicit-Arguments）" class="headerlink" title="隐式参数（Implicit Arguments）"></a>隐式参数（Implicit Arguments）</h4><p>类型参数的推断还是复杂，我们希望避免写 _。</p>
<p>Arguments 用于指令指定函数或构造子的名字并列出其参数名， 花括号中的任何参数都会被视作隐式参数。</p>
<figure class="highlight plaintext"><table><tr><td class="gutter"><pre><span class="line">1</span><br><span class="line">2</span><br><span class="line">3</span><br></pre></td><td class="code"><pre><span class="line">Arguments nil &#123;X&#125;.</span><br><span class="line">Arguments cons &#123;X&#125; _ _.</span><br><span class="line">Arguments repeat &#123;X&#125; x count.</span><br></pre></td></tr></table></figure>

<p>我们还可以在定义函数时就声明隐式参数， 只需要将某个参数两边的圆括号换成花括号</p>
<figure class="highlight plaintext"><table><tr><td class="gutter"><pre><span class="line">1</span><br><span class="line">2</span><br><span class="line">3</span><br><span class="line">4</span><br><span class="line">5</span><br></pre></td><td class="code"><pre><span class="line">Fixpoint repeat&#x27;&#x27;&#x27; &#123;X : Type&#125; (x : X) (count : nat) : list X :=</span><br><span class="line">  match count with</span><br><span class="line">  | 0 ⇒ nil</span><br><span class="line">  | S count&#x27; ⇒ cons x (repeat&#x27;&#x27;&#x27; x count&#x27;)</span><br><span class="line">  end.</span><br></pre></td></tr></table></figure>

<figure class="highlight plaintext"><table><tr><td class="gutter"><pre><span class="line">1</span><br><span class="line">2</span><br><span class="line">3</span><br></pre></td><td class="code"><pre><span class="line">Inductive list&#x27; &#123;X:Type&#125; : Type :=</span><br><span class="line">  | nil&#x27;</span><br><span class="line">  | cons&#x27; (x : X) (l : list&#x27;).</span><br></pre></td></tr></table></figure>



<h4 id="显式提供类型参数"><a href="#显式提供类型参数" class="headerlink" title="显式提供类型参数"></a>显式提供类型参数</h4><p>有的时候，Coq判断不出具体的类型，需要直接明确。</p>
<figure class="highlight plaintext"><table><tr><td class="gutter"><pre><span class="line">1</span><br></pre></td><td class="code"><pre><span class="line">Fail Definition mynil := nil.</span><br></pre></td></tr></table></figure>

<p>可以通过两种方法进行处理这个问题。</p>
<p>第一种是通过显示指定目标的类型，使得coq能够进行自动推导</p>
<p><code>Definition mynil : list nat := nil.</code><br>第二种是使用@来暂时性地禁用隐式参数，从而显示的给出参数</p>
<p><code>Definition mynil&#39; := @nil nat.</code></p>
<h3 id="2-多态序对"><a href="#2-多态序对" class="headerlink" title="2.  多态序对"></a>2.  多态序对</h3><figure class="highlight plaintext"><table><tr><td class="gutter"><pre><span class="line">1</span><br><span class="line">2</span><br><span class="line">3</span><br><span class="line">4</span><br></pre></td><td class="code"><pre><span class="line">Inductive prod (X Y : Type) : Type :=</span><br><span class="line">| pair (x : X) (y : Y).</span><br><span class="line"></span><br><span class="line">Arguments pair &#123;X&#125; &#123;Y&#125;.</span><br></pre></td></tr></table></figure>

<p>prod是类型，pair 1 2 是 prod类型的数据</p>
<h3 id="3-多态候选"><a href="#3-多态候选" class="headerlink" title="3.  多态候选"></a>3.  多态候选</h3><figure class="highlight plaintext"><table><tr><td class="gutter"><pre><span class="line">1</span><br><span class="line">2</span><br><span class="line">3</span><br><span class="line">4</span><br><span class="line">5</span><br><span class="line">6</span><br></pre></td><td class="code"><pre><span class="line">Inductive option (X:Type) : Type :=</span><br><span class="line">  | Some (x : X)</span><br><span class="line">  | None.</span><br><span class="line"></span><br><span class="line">Arguments Some &#123;X&#125;.</span><br><span class="line">Arguments None &#123;X&#125;.</span><br></pre></td></tr></table></figure>



<h2 id="函数作为数据（Functions-as-Data）"><a href="#函数作为数据（Functions-as-Data）" class="headerlink" title="函数作为数据（Functions as Data）"></a>函数作为数据（Functions as Data）</h2><p>接收函数作为参数或者使用函数作为返回值的函数称为高阶函数*(Higher-Order Functions)*. 常见的高阶函数包括了<code>filter</code>, <code>map</code>, <code>flat_map</code>, <code>fold</code>等等</p>
<h3 id="1-filter"><a href="#1-filter" class="headerlink" title="1. filter"></a>1. filter</h3><p>函数<code>filter</code>接收一个函数<code>test</code>，以及一个<code>list</code>，其将<code>list</code>中的每个元素作为参数分别执行<code>test</code>，根据<code>test</code>执行结果来保留其中一部分元素（<code>test</code>执行结果为<code>true</code>的元素）</p>
<figure class="highlight plaintext"><table><tr><td class="gutter"><pre><span class="line">1</span><br><span class="line">2</span><br><span class="line">3</span><br><span class="line">4</span><br><span class="line">5</span><br><span class="line">6</span><br><span class="line">7</span><br><span class="line">8</span><br></pre></td><td class="code"><pre><span class="line">Fixpoint filter &#123;X:Type&#125; (test: X-&gt;bool) (l:list X) : (list X) :=</span><br><span class="line">  match l with</span><br><span class="line">  | [] =&gt; []</span><br><span class="line">  | h :: t =&gt;</span><br><span class="line">    if test h then h :: (filter test t)</span><br><span class="line">    else filter test t</span><br><span class="line">  end.</span><br><span class="line"></span><br></pre></td></tr></table></figure>



<h3 id="2-map"><a href="#2-map" class="headerlink" title="2. map"></a>2. map</h3><p>函数<code>map</code>接收一个函数<code>f</code>以及一个<code>list</code>，将<code>list</code>中的元素逐个使用<code>f</code>进行转换。</p>
<figure class="highlight plaintext"><table><tr><td class="gutter"><pre><span class="line">1</span><br><span class="line">2</span><br></pre></td><td class="code"><pre><span class="line">输入 f [ a b c d e]</span><br><span class="line">输出 [ f(a) f(b) f(c) f(d) f(e)]</span><br></pre></td></tr></table></figure>

<figure class="highlight plaintext"><table><tr><td class="gutter"><pre><span class="line">1</span><br><span class="line">2</span><br><span class="line">3</span><br><span class="line">4</span><br><span class="line">5</span><br></pre></td><td class="code"><pre><span class="line">Fixpoint map &#123;X Y: Type&#125; (f:X-&gt;Y) (l:list X) : (list Y) :=</span><br><span class="line">  match l with</span><br><span class="line">  | []     =&gt; []</span><br><span class="line">  | h :: t =&gt; (f h) :: (map f t)</span><br><span class="line">  end.</span><br></pre></td></tr></table></figure>



<h3 id="3-fold"><a href="#3-fold" class="headerlink" title="3. fold"></a>3. fold</h3><p>函数<code>fold</code>接收一个函数<code>f</code>，一个<code>list</code>以及一个初始值<code>i</code>，其将<code>list</code>中的元素作为函数<code>f</code>的第一个参数传入，将上一个调用<code>f</code>的结果作为<code>f</code>的第二个参数传入，对<code>list</code>中的元素进行逐个处理，并将最后一次调用<code>f</code>得到的结果作为返回值返回。</p>
<figure class="highlight plaintext"><table><tr><td class="gutter"><pre><span class="line">1</span><br><span class="line">2</span><br></pre></td><td class="code"><pre><span class="line">输入 f [a b c] i</span><br><span class="line">输出 f(c, f(b, f(a, i)))</span><br></pre></td></tr></table></figure>

<figure class="highlight plaintext"><table><tr><td class="gutter"><pre><span class="line">1</span><br><span class="line">2</span><br><span class="line">3</span><br><span class="line">4</span><br><span class="line">5</span><br><span class="line">6</span><br><span class="line">7</span><br></pre></td><td class="code"><pre><span class="line">Fixpoint fold &#123;X Y: Type&#125; (f: X-&gt;Y-&gt;Y) (l: list X) (b: Y)</span><br><span class="line">                         : Y :=</span><br><span class="line">  match l with</span><br><span class="line">  | nil =&gt; b</span><br><span class="line">  | h :: t =&gt; f h (fold f t b)</span><br><span class="line">  end.</span><br><span class="line"></span><br></pre></td></tr></table></figure>

<h3 id="4-匿名函数-Anonymous-Functions"><a href="#4-匿名函数-Anonymous-Functions" class="headerlink" title="4. 匿名函数(Anonymous Functions)"></a>4. 匿名函数(Anonymous Functions)</h3><p>某些短小的，特定的函数可能不需要为其定义一个名称，此时可以使用匿名函数来定义, 匿名函数使用关键字<code>fun</code>来定义</p>
<figure class="highlight plaintext"><table><tr><td class="gutter"><pre><span class="line">1</span><br></pre></td><td class="code"><pre><span class="line">fun l =&gt; (length l) =? 1)</span><br></pre></td></tr></table></figure>

<figure class="highlight plaintext"><table><tr><td class="gutter"><pre><span class="line">1</span><br><span class="line">2</span><br><span class="line">3</span><br><span class="line">4</span><br><span class="line">5</span><br><span class="line">6</span><br></pre></td><td class="code"><pre><span class="line">Example test_filter2&#x27;:</span><br><span class="line">    filter (fun l =&gt; (length l) =? 1)</span><br><span class="line">           [ [1; 2]; [3]; [4]; [5;6;7]; []; [8] ]</span><br><span class="line">  = [ [3]; [4]; [8] ].</span><br><span class="line">Proof. reflexivity. Qed.</span><br><span class="line"></span><br></pre></td></tr></table></figure>

<p>值得注意的是，无论是filter还是map，所调用的函数均是处理子元素的</p>
<h2 id="Exercises"><a href="#Exercises" class="headerlink" title="Exercises"></a>Exercises</h2><h3 id="1-Exercise-2-stars-standard-fold-length"><a href="#1-Exercise-2-stars-standard-fold-length" class="headerlink" title="1. Exercise: 2 stars, standard (fold_length)"></a>1. Exercise: 2 stars, standard (fold_length)</h3><p>（证明列表问题，通常采用的是归纳的方法。）</p>
<p> 非形式化证明：</p>
   <figure class="highlight plaintext"><table><tr><td class="gutter"><pre><span class="line">1</span><br><span class="line">2</span><br><span class="line">3</span><br><span class="line">4</span><br><span class="line">5</span><br><span class="line">6</span><br><span class="line">7</span><br><span class="line">8</span><br><span class="line">9</span><br><span class="line">10</span><br><span class="line">11</span><br><span class="line">12</span><br></pre></td><td class="code"><pre><span class="line">&#x27;定理&#x27;：对所有类型的列表 l，fold_length l = lenght l.</span><br><span class="line"> &#x27;证明&#x27;: 通过对 l 使用归纳法。</span><br><span class="line"> 首先, 假设 l= []。我们必须证明：</span><br><span class="line">      fold_length [] = lenght [].</span><br><span class="line"> 这可以通过展开 fold_length 和 lenght 的定义得到。</span><br><span class="line">   然后, 假设 l = x::l&#x27;，有：</span><br><span class="line">    	fold_length l&#x27; = lenght l&#x27;.</span><br><span class="line"> （归纳假设）。我们必须证明：</span><br><span class="line">     fold_length (x::l&#x27;) = lenght (x::l&#x27;).</span><br><span class="line"> 根据 length 的定义 , 上式等价于：</span><br><span class="line">     fold_length (x::l&#x27;) = 1 +lenght (l&#x27;).   </span><br><span class="line"> 该式可通过我们的归纳假设立即证得</span><br></pre></td></tr></table></figure>

   <figure class="highlight plaintext"><table><tr><td class="gutter"><pre><span class="line">1</span><br><span class="line">2</span><br><span class="line">3</span><br><span class="line">4</span><br><span class="line">5</span><br><span class="line">6</span><br><span class="line">7</span><br><span class="line">8</span><br></pre></td><td class="code"><pre><span class="line">Theorem fold_length_correct : forall X (l : list X),</span><br><span class="line">   fold_length l = length l.</span><br><span class="line">   </span><br><span class="line"> Proof.</span><br><span class="line">   intros. induction l.</span><br><span class="line">   - reflexivity.</span><br><span class="line">   - simpl. rewrite &lt;- IHl. reflexivity.</span><br><span class="line"> Qed.</span><br></pre></td></tr></table></figure>

<h3 id="2-Exercise-2-stars-advanced-currying"><a href="#2-Exercise-2-stars-advanced-currying" class="headerlink" title="2. Exercise: 2 stars, advanced (currying)"></a>2. Exercise: 2 stars, advanced (currying)</h3><blockquote>
<p>It is possible to convert a function between these two types. Converting from X × Y → Z to X → Y → Z is called <em>currying</em>, in honor of the logician Haskell Curry. Converting from X → Y → Z to X × Y → Z is called <em>uncurrying</em>.</p>
</blockquote>
<p>   在 Coq 中，函数 f : A → B → C 的类型其实是 A → (B → C)。 也就是说，如果给 f 一个类型为 A 的值，它就会给你函数 f’ : B → C。 如果再给 f’ 一个类型为 B 的值，它就会返回一个类型为 C 的值。</p>
  <figure class="highlight plaintext"><table><tr><td class="gutter"><pre><span class="line">1</span><br><span class="line">2</span><br><span class="line">3</span><br><span class="line">4</span><br><span class="line">5</span><br></pre></td><td class="code"><pre><span class="line">Definition prod_curry &#123;X Y Z : Type&#125;</span><br><span class="line">  (f : X × Y → Z) (x : X) (y : Y) : Z := f (x, y).</span><br><span class="line">  </span><br><span class="line">Definition prod_uncurry &#123;X Y Z : Type&#125;</span><br><span class="line">  (f : X → Y → Z) (p : X × Y) : Z := f (fst p) (snd p). </span><br></pre></td></tr></table></figure>

   <figure class="highlight plaintext"><table><tr><td class="gutter"><pre><span class="line">1</span><br><span class="line">2</span><br><span class="line">3</span><br><span class="line">4</span><br><span class="line">5</span><br><span class="line">6</span><br><span class="line">7</span><br><span class="line">8</span><br><span class="line">9</span><br><span class="line">10</span><br><span class="line">11</span><br><span class="line">12</span><br><span class="line">13</span><br></pre></td><td class="code"><pre><span class="line">Theorem uncurry_curry : forall (X Y Z : Type)</span><br><span class="line">                        (f : X -&gt; Y -&gt; Z)</span><br><span class="line">                        x y,</span><br><span class="line">  prod_curry (prod_uncurry f) x y = f x y.</span><br><span class="line">Proof.</span><br><span class="line">  intros. reflexivity. Qed.</span><br><span class="line"></span><br><span class="line">Theorem curry_uncurry : forall (X Y Z : Type)</span><br><span class="line">                        (f : (X * Y) -&gt; Z) (p : X * Y),</span><br><span class="line">  prod_uncurry (prod_curry f) p = f p.</span><br><span class="line">Proof.</span><br><span class="line">  intros. destruct p. simpl. reflexivity.</span><br><span class="line"> Qed.</span><br></pre></td></tr></table></figure>

<h3 id="3-Church-Numerals-Advanced"><a href="#3-Church-Numerals-Advanced" class="headerlink" title="3. Church Numerals (Advanced)"></a>3. Church Numerals (Advanced)</h3><p>   我们可以将自然数 n 表示为一个函数， 它接受一个函数 f 作为参数并返回迭代了 n 次的 f</p>
<figure class="highlight plaintext"><table><tr><td class="gutter"><pre><span class="line">1</span><br><span class="line">2</span><br><span class="line">3</span><br><span class="line">4</span><br><span class="line">5</span><br><span class="line">6</span><br><span class="line">7</span><br><span class="line">8</span><br><span class="line">9</span><br><span class="line">10</span><br><span class="line">11</span><br><span class="line">12</span><br><span class="line">13</span><br><span class="line">14</span><br><span class="line">15</span><br><span class="line">16</span><br><span class="line">17</span><br><span class="line">18</span><br><span class="line">19</span><br><span class="line">20</span><br><span class="line">21</span><br><span class="line">22</span><br><span class="line">23</span><br></pre></td><td class="code"><pre><span class="line">Module Church.</span><br><span class="line">Definition cnat := forall X : Type, (X -&gt; X) -&gt; X -&gt; X.</span><br><span class="line"></span><br><span class="line">(** Let&#x27;s see how to write some numbers with this notation. Iterating</span><br><span class="line">    a function once should be the same as just applying it.  Thus: *)</span><br><span class="line"></span><br><span class="line">Definition one : cnat :=</span><br><span class="line">  fun (X : Type) (f : X -&gt; X) (x : X) =&gt; f x.</span><br><span class="line"></span><br><span class="line">(** Similarly, [two] should apply [f] twice to its argument: *)</span><br><span class="line"></span><br><span class="line">Definition two : cnat :=</span><br><span class="line">  fun (X : Type) (f : X -&gt; X) (x : X) =&gt; f (f x).</span><br><span class="line"></span><br><span class="line">(** Defining [zero] is somewhat trickier: how can we &quot;apply a function</span><br><span class="line">    zero times&quot;?  The answer is actually simple: just return the</span><br><span class="line">    argument untouched. *)</span><br><span class="line"></span><br><span class="line">Definition zero : cnat :=</span><br><span class="line">  fun (X : Type) (f : X -&gt; X) (x : X) =&gt; x.</span><br><span class="line">  </span><br><span class="line">Definition three : cnat := @doit3times.</span><br><span class="line"></span><br></pre></td></tr></table></figure>

<p><strong>Exercise: 2 stars, advanced (church_scc)</strong></p>
<p>自然数的后继：给定一个邱奇数 n，它的后继 succ n 是一个把它的参数比 n 还多迭代一次的函数。</p>
<p>解析：n作为cnat类型的数据，实际上就是一个函数</p>
<figure class="highlight plaintext"><table><tr><td class="gutter"><pre><span class="line">1</span><br><span class="line">2</span><br><span class="line">3</span><br><span class="line">4</span><br><span class="line">5</span><br><span class="line">6</span><br><span class="line">7</span><br><span class="line">8</span><br><span class="line">9</span><br><span class="line">10</span><br><span class="line">11</span><br><span class="line">12</span><br></pre></td><td class="code"><pre><span class="line">Definition scc (n : cnat) : cnat :=</span><br><span class="line">  fun (X : Type) (f : X -&gt; X) (x : X) =&gt; n X f (f x).</span><br><span class="line"></span><br><span class="line">Example scc_1 : scc zero = one.</span><br><span class="line">Proof. reflexivity. Qed.</span><br><span class="line"></span><br><span class="line">Example scc_2 : scc one = two.</span><br><span class="line">Proof. reflexivity. Qed.</span><br><span class="line"></span><br><span class="line">Example scc_3 : scc two = three.</span><br><span class="line">Proof. reflexivity. Qed.</span><br><span class="line"></span><br></pre></td></tr></table></figure>



<p><strong>Exercise: 3 stars, advanced (church_plus)</strong></p>
<p>两邱奇数相加：</p>
<figure class="highlight plaintext"><table><tr><td class="gutter"><pre><span class="line">1</span><br><span class="line">2</span><br><span class="line">3</span><br><span class="line">4</span><br><span class="line">5</span><br><span class="line">6</span><br><span class="line">7</span><br><span class="line">8</span><br><span class="line">9</span><br><span class="line">10</span><br><span class="line">11</span><br><span class="line">12</span><br><span class="line">13</span><br></pre></td><td class="code"><pre><span class="line">Definition plus (n m : cnat) : cnat := </span><br><span class="line">	fun (X : Type) (f : X -&gt; X) (x : X) =&gt;  n X f (m X f x) .</span><br><span class="line"></span><br><span class="line">Example plus_1 : plus zero one = one.</span><br><span class="line">Proof. reflexivity. Qed.</span><br><span class="line"></span><br><span class="line">Example plus_2 : plus two three = plus three two.</span><br><span class="line">Proof. reflexivity. Qed.</span><br><span class="line"></span><br><span class="line">Example plus_3 :</span><br><span class="line">  plus (plus two two) three = plus one (plus three three).</span><br><span class="line">Proof. reflexivity. Qed.</span><br><span class="line"></span><br></pre></td></tr></table></figure>



<p>**Exercise: 3 stars, advanced (church_mult) **(不理解)</p>
<figure class="highlight plaintext"><table><tr><td class="gutter"><pre><span class="line">1</span><br><span class="line">2</span><br><span class="line">3</span><br><span class="line">4</span><br><span class="line">5</span><br><span class="line">6</span><br><span class="line">7</span><br><span class="line">8</span><br><span class="line">9</span><br><span class="line">10</span><br><span class="line">11</span><br><span class="line">12</span><br></pre></td><td class="code"><pre><span class="line">Definition mult (n m : cnat) : cnat :=</span><br><span class="line">  fun (X : Type) (f : X -&gt; X) =&gt; m X (n X f).</span><br><span class="line"></span><br><span class="line">Example mult_1 : mult one one = one.</span><br><span class="line">Proof. reflexivity. Qed.</span><br><span class="line"></span><br><span class="line">Example mult_2 : mult zero (plus three three) = zero.</span><br><span class="line">Proof. reflexivity. Qed.</span><br><span class="line"></span><br><span class="line">Example mult_3 : mult two three = plus three three.</span><br><span class="line">Proof. reflexivity. Qed.</span><br><span class="line"></span><br></pre></td></tr></table></figure>



<p><strong>Exercise: 3 stars, advanced (church_exp)</strong></p>
<p>乘方：</p>
<p>（*’提示’*：多态在这里起到了关键的作用。然而，棘手之处在于选择正确的类型来迭代。 如果你遇到了「Universe inconsistency，全域不一致」错误，请在不同的类型上迭 代。在 cnat 本身上迭代通常会有问题。）</p>

    </div>

    
    
    

    <footer class="post-footer">

        

          <div class="post-nav">
            <div class="post-nav-item">
                <a href="/blog/2023/07/18/SF-1-Lists/" rel="prev" title="SF-1-Lists">
                  <i class="fa fa-chevron-left"></i> SF-1-Lists
                </a>
            </div>
            <div class="post-nav-item">
                <a href="/blog/2023/07/19/SF-1-Tactics/" rel="next" title="SF-1-Tactics">
                  SF-1-Tactics <i class="fa fa-chevron-right"></i>
                </a>
            </div>
          </div>
    </footer>
  </article>
</div>






</div>
  </main>

  <footer class="footer">
    <div class="footer-inner">


<div class="copyright">
  &copy; 
  <span itemprop="copyrightYear">2023</span>
  <span class="with-love">
    <i class="fa fa-heart"></i>
  </span>
  <span class="author" itemprop="copyrightHolder">yanlw</span>
</div>
<div class="busuanzi-count">
    <span class="post-meta-item" id="busuanzi_container_site_uv">
      <span class="post-meta-item-icon">
        <i class="fa fa-user"></i>
      </span>
      <span class="site-uv" title="总访客量">
        <span id="busuanzi_value_site_uv"></span>
      </span>
    </span>
    <span class="post-meta-item" id="busuanzi_container_site_pv">
      <span class="post-meta-item-icon">
        <i class="fa fa-eye"></i>
      </span>
      <span class="site-pv" title="总访问量">
        <span id="busuanzi_value_site_pv"></span>
      </span>
    </span>
</div>
  <div class="powered-by">由 <a href="https://hexo.io/" rel="noopener" target="_blank">Hexo</a> & <a href="https://theme-next.js.org/pisces/" rel="noopener" target="_blank">NexT.Pisces</a> 强力驱动
  </div>

    </div>
  </footer>

  
  <div class="reading-progress-bar"></div>

  <a href="https://gitee.com/yanlwsometing" class="github-corner" title="在 GitHub 上关注我" aria-label="在 GitHub 上关注我" rel="noopener" target="_blank"><svg width="80" height="80" viewBox="0 0 250 250" aria-hidden="true"><path d="M0,0 L115,115 L130,115 L142,142 L250,250 L250,0 Z"></path><path d="M128.3,109.0 C113.8,99.7 119.0,89.6 119.0,89.6 C122.0,82.7 120.5,78.6 120.5,78.6 C119.2,72.0 123.4,76.3 123.4,76.3 C127.3,80.9 125.5,87.3 125.5,87.3 C122.9,97.6 130.6,101.9 134.4,103.2" fill="currentColor" style="transform-origin: 130px 106px;" class="octo-arm"></path><path d="M115.0,115.0 C114.9,115.1 118.7,116.5 119.8,115.4 L133.7,101.6 C136.9,99.2 139.9,98.4 142.2,98.6 C133.8,88.0 127.5,74.4 143.8,58.0 C148.5,53.4 154.0,51.2 159.7,51.0 C160.3,49.4 163.2,43.6 171.4,40.1 C171.4,40.1 176.1,42.5 178.8,56.2 C183.1,58.6 187.2,61.8 190.9,65.4 C194.5,69.0 197.7,73.2 200.1,77.6 C213.8,80.2 216.3,84.9 216.3,84.9 C212.7,93.1 206.9,96.0 205.4,96.6 C205.1,102.4 203.0,107.8 198.3,112.5 C181.9,128.9 168.3,122.5 157.7,114.1 C157.9,116.9 156.7,120.9 152.7,124.9 L141.0,136.5 C139.8,137.7 141.6,141.9 141.8,141.8 Z" fill="currentColor" class="octo-body"></path></svg></a>

<noscript>
  <div class="noscript-warning">Theme NexT works best with JavaScript enabled</div>
</noscript>


  
  <script src="https://cdnjs.cloudflare.com/ajax/libs/animejs/3.2.1/anime.min.js" integrity="sha256-XL2inqUJaslATFnHdJOi9GfQ60on8Wx1C2H8DYiN1xY=" crossorigin="anonymous"></script>
  <script src="https://cdnjs.cloudflare.com/ajax/libs/jquery/3.6.4/jquery.min.js" integrity="sha256-oP6HI9z1XaZNBrJURtCoUT5SUnxFr8s3BzRl+cbzUq8=" crossorigin="anonymous"></script>
  <script src="https://cdnjs.cloudflare.com/ajax/libs/fancybox/3.5.7/jquery.fancybox.min.js" integrity="sha256-yt2kYMy0w8AbtF89WXb2P1rfjcP/HTHLT7097U8Y5b8=" crossorigin="anonymous"></script>
<script src="/blog/js/comments.js"></script><script src="/blog/js/utils.js"></script><script src="/blog/js/next-boot.js"></script>

  


  <script src="/blog/js/third-party/fancybox.js"></script>



  
  <script async src="https://busuanzi.ibruce.info/busuanzi/2.3/busuanzi.pure.mini.js"></script>





</body>
</html>
